metamodel automata  {

    class automaton 
        { 
            attribute trace : string;
            reference active : state [1 - 1];
        }

    class transition
        {
            attribute label : string;
            reference orig : state [1 - 1] oppositeOf out;
            reference dest : state [1 - 1] oppositeOf inp;
        }

    class state 
        {
            reference inp : transition oppositeOf dest;
            reference out : transition oppositeOf orig;
        }  

    class initialState extends state { }

}
constraints{
allInstances(initialState).size() == 2;
allInstances(transition)->forAll(tr | not(tr.label == ""));
allInstances(state)
 ->forAll(st | st.out ->forAll(tr1 | st.out ->forAll( tr2 | (tr1.label == tr2.label) implies (tr1 == tr2))));
}
		  

